Inference at * 1 1 0 
Iof proof for Lemma absval eq:



1. x : 
2. y : 
  (if 0 z x then x else -x fi  = if 0 z y then y else -y fi )  x =  y 

latex

 by InteriorProof PERMUTE{1:n,
 by InteriorProof PERMUTE{2:n,
 by InteriorProof PERMUTE{3:n,
 by InteriorProof PERMUTE{4:n,
 by InteriorProof PERMUTE{5:n,
 by InteriorProof PERMUTE{6:n,
 by InteriorProof PERMUTE{7:n,
 by InteriorProof PERMUTE{8:n,
 by InteriorProof PERMUTE{9:n,
 by InteriorProof PERMUTE{10:n,
 by InteriorProof PERMUTE{11:n,
 by InteriorProof PERMUTE{12:n,
 by InteriorProof PERMUTE{13:n,
 by InteriorProof PERMUTE{14:n,
 by InteriorProof PERMUTE{15:n,
 by InteriorProof PERMUTE{16:n,
 by InteriorProof PERMUTE{17:n,
 by InteriorProof PERMUTE{18:n,
 by InteriorProof PERMUTE{19:n,
 by InteriorProof PERMUTE{20:n,
 by InteriorProof PERMUTE{18:n,
 by InteriorProof PERMUTE{21:n,
 by InteriorProof PERMUTE{19:n,
 by InteriorProof PERMUTE{22:n,
 by InteriorProof PERMUTE{23:n,
 by InteriorProof PERMUTE{24:n,
 by InteriorProof PERMUTE{25:n,
 by InteriorProof PERMUTE{26:n,
 by InteriorProof PERMUTE{24:n,
 by InteriorProof PERMUTE{23:n,
 by InteriorProof PERMUTE{27:n,
 by InteriorProof PERMUTE{28:n,
 by InteriorProof PERMUTE{29:n,
 by InteriorProof PERMUTE{30:n,
 by InteriorProof PERMUTE{31:n,
 by InteriorProof PERMUTE{32:n,
 by InteriorProof PERMUTE{33:n,
 by InteriorProof PERMUTE{34:n,
 by InteriorProof PERMUTE{35:n,
 by InteriorProof PERMUTE{36:n,
 by InteriorProof PERMUTE{37:n,
 by InteriorProof PERMUTE{38:n,
 by InteriorProof PERMUTE{39:n,
 by InteriorProof PERMUTE{40:n,
 by InteriorProof PERMUTE{41:n,
 by InteriorProof PERMUTE{42:n,
 by InteriorProof PERMUTE{43:n,
 by InteriorProof PERMUTE{44:n,
 by InteriorProof PERMUTE{45:n,
 by InteriorProof PERMUTE{46:n,
 by InteriorProof PERMUTE{47:n,
 by InteriorProof PERMUTE{48:n,
 by InteriorProof PERMUTE{46:n,
 by InteriorProof PERMUTE{49:n,
 by InteriorProof PERMUTE{47:n,
 by InteriorProof PERMUTE{50:n,
 by InteriorProof PERMUTE{51:n,
 by InteriorProof PERMUTE{52:n,
 by InteriorProof PERMUTE{53:n,
 by InteriorProof PERMUTE{54:n,
 by InteriorProof PERMUTE{52:n,
 by InteriorProof PERMUTE{51:n,
 by InteriorProof PERMUTE{55:n} 

latex

 1: .....wf..... NILNIL

 1:   0 z x  
 2: .....wf..... NILNIL

 2:     Type
 3: .....wf..... NILNIL

 3: 3. 0 z x = tt
 3:   (0 z x = tt)  
 4: .....wf..... NILNIL

 4: 3. 0 z x = tt
 4:   (0 z x)  
 5: .....wf..... NILNIL

 5: 3. 0 z x = tt
 5:   (0  x)  
 6: .....wf..... NILNIL

 6: 3. 0 z x = tt
 6:   0 z x  
 7: .....wf..... NILNIL

 7: 3. 0 z x = tt
 7:   0  
 8: .....wf..... NILNIL

 8: 3. 0 z x = tt
 8:   x  
 9: .....wf..... NILNIL

 9: 3. 0  x
 9:   0 z y  
 10: .....wf..... NILNIL

 10: 3. 0  x
 10:     Type
 11: .....wf..... NILNIL

 11: 3. 0  x
 11: 4. 0 z y = tt
 11:   (0 z y = tt)  
 12: .....wf..... NILNIL

 12: 3. 0  x
 12: 4. 0 z y = tt
 12:   (0 z y)  
 13: .....wf..... NILNIL

 13: 3. 0  x
 13: 4. 0 z y = tt
 13:   (0  y)  
 14: .....wf..... NILNIL

 14: 3. 0  x
 14: 4. 0 z y = tt
 14:   0 z y  
 15: .....wf..... NILNIL

 15: 3. 0  x
 15: 4. 0 z y = tt
 15:   0  
 16: .....wf..... NILNIL

 16: 3. 0  x
 16: 4. 0 z y = tt
 16:   y  
 17: 

 17: 3. 0  x
 17: 4. 0  y
 17:   (if tt then x else -x fi  = if tt then y else -y fi )  x =  y
 18: .....wf..... NILNIL

 18: 3. 0  x
 18: 4. 0 z y = ff
 18:   (0 z y = ff)  
 19: .....wf..... NILNIL

 19: 3. 0  x
 19: 4. 0 z y = ff
 19:   (y <z 0)  
 20: .....wf..... NILNIL

 20: 3. 0  x
 20: 4. 0 z y = ff
 20:   (y < 0)  
 21: .....wf..... NILNIL

 21: 3. 0  x
 21: 4. 0 z y = ff
 21:   ((0 z y))  
 22: .....wf..... NILNIL

 22: 3. 0  x
 22: 4. 0 z y = ff
 22:   0 z y  
 23: .....wf..... NILNIL

 23: 3. 0  x
 23: 4. 0 z y = ff
 23:   0  
 24: .....wf..... NILNIL

 24: 3. 0  x
 24: 4. 0 z y = ff
 24:   y  
 25: .....antecedent..... NILNIL

 25: 3. 0  x
 25: 4. 0 z y = ff
 25:   True
 26: .....wf..... NILNIL

 26: 3. 0  x
 26: 4. 0 z y = ff
 26: 5. ((0 z y)) = (y <z 0)
 26:    = 
 27: 

 27: 3. 0  x
 27: 4. y < 0
 27:   (if tt then x else -x fi  = if ff then y else -y fi )  x =  y
 28: .....wf..... NILNIL

 28: 3. 0 z x = ff
 28:   (0 z x = ff)  
 29: .....wf..... NILNIL

 29: 3. 0 z x = ff
 29:   (x <z 0)  
 30: .....wf..... NILNIL

 30: 3. 0 z x = ff
 30:   (x < 0)  
 31: .....wf..... NILNIL

 31: 3. 0 z x = ff
 31:   ((0 z x))  
 32: .....wf..... NILNIL

 32: 3. 0 z x = ff
 32:   0 z x  
 33: .....wf..... NILNIL

 33: 3. 0 z x = ff
 33:   0  
 34: .....wf..... NILNIL

 34: 3. 0 z x = ff
 34:   x  
 35: .....antecedent..... NILNIL

 35: 3. 0 z x = ff
 35:   True
 36: .....wf..... NILNIL

 36: 3. 0 z x = ff
 36: 4. ((0 z x)) = (x <z 0)
 36:    = 
 37: .....wf..... NILNIL

 37: 3. x < 0
 37:   0 z y  
 38: .....wf..... NILNIL

 38: 3. x < 0
 38:     Type
 39: .....wf..... NILNIL

 39: 3. x < 0
 39: 4. 0 z y = tt
 39:   (0 z y = tt)  
 40: .....wf..... NILNIL

 40: 3. x < 0
 40: 4. 0 z y = tt
 40:   (0 z y)  
 41: .....wf..... NILNIL

 41: 3. x < 0
 41: 4. 0 z y = tt
 41:   (0  y)  
 42: .....wf..... NILNIL

 42: 3. x < 0
 42: 4. 0 z y = tt
 42:   0 z y  
 43: .....wf..... NILNIL

 43: 3. x < 0
 43: 4. 0 z y = tt
 43:   0  
 44: .....wf..... NILNIL

 44: 3. x < 0
 44: 4. 0 z y = tt
 44:   y  
 45: 

 45: 3. x < 0
 45: 4. 0  y
 45:   (if ff then x else -x fi  = if tt then y else -y fi )  x =  y
 46: .....wf..... NILNIL

 46: 3. x < 0
 46: 4. 0 z y = ff
 46:   (0 z y = ff)  
 47: .....wf..... NILNIL

 47: 3. x < 0
 47: 4. 0 z y = ff
 47:   (y <z 0)  
 48: .....wf..... NILNIL

 48: 3. x < 0
 48: 4. 0 z y = ff
 48:   (y < 0)  
 49: .....wf..... NILNIL

 49: 3. x < 0
 49: 4. 0 z y = ff
 49:   ((0 z y))  
 50: .....wf..... NILNIL

 50: 3. x < 0
 50: 4. 0 z y = ff
 50:   0 z y  
 51: .....wf..... NILNIL

 51: 3. x < 0
 51: 4. 0 z y = ff
 51:   0  
 52: .....wf..... NILNIL

 52: 3. x < 0
 52: 4. 0 z y = ff
 52:   y  
 53: .....antecedent..... NILNIL

 53: 3. x < 0
 53: 4. 0 z y = ff
 53:   True
 54: .....wf..... NILNIL

 54: 3. x < 0
 54: 4. 0 z y = ff
 54: 5. ((0 z y)) = (y <z 0)
 54:    = 
 55: 

 55: 3. x < 0
 55: 4. y < 0
 55:   (if ff then x else -x fi  = if ff then y else -y fi )  x =  y
 .

Definitions	{x:A| B(x)} , x.A(x), b, i <z j, a < b, ff, inr x , x:A  B(x), b, f(a), , Ax, inl x , left + right, x:AB(x), Type, i =  j, i z j, -n, tt, if b then t else f fi , s = t, #$n, A  B, , , Unit, , True, T, P  Q, P & Q, P  Q, x:A. B(x), t  T, P  Q
Lemmas	bool wf, true wf, squash wf, assert of lt int, bnot of le int, assert wf, eqff to assert, assert of le int, eqtt to assert, iff transitivity